/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRK30



␈↓ ↓H␈↓α␈↓ ¬areply to Burger

␈↓ ↓H␈↓␈↓ α_My␈α␈↓↓samefringe␈↓␈αincludes␈αall␈αatoms␈αin␈α
an␈αS-expression␈αwhile␈αBurger's␈αomits␈αthe␈αNILs␈α
at␈αthe
␈↓ ↓H␈↓ends of lists.  Mine corresponds to the definition

␈↓ ↓H␈↓1)␈↓ α8  ␈↓↓fringe x ← ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ <x> ␈↓αelse␈↓↓ fringe ␈↓αa␈↓↓ x * fringe ␈↓αd␈↓↓ x␈↓,

␈↓ ↓H␈↓where␈α*␈αis␈αan␈αinfix␈αfor␈αthe␈αassociative␈αoperation␈α␈↓↓append␈↓.␈α Using␈αthe␈αresults␈αof␈α(Cartwright␈α1977),
␈↓ ↓H␈↓we can characterize ␈↓↓gopher␈↓ by the sentence

␈↓ ↓H␈↓2)␈↓ α8  ␈↓↓∀x.(gopher x = ␈↓αif␈↓↓ ␈↓αat␈↓↓ ␈↓αa␈↓↓ x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ gopher[␈↓αaa␈↓↓ x .[␈↓αda␈↓↓ x . ␈↓αd␈↓↓ x]])␈↓

␈↓ ↓H␈↓of␈αfirst␈α
order␈αlogic.␈α
 (Conditional␈αexpressions␈α
are␈αadmitted␈αas␈α
terms␈αas␈α
in␈α(Manna␈α
1974),␈αand␈αthe␈α
␈↓↓a
␈↓ ↓H␈↓↓priori␈↓␈αpossibility␈αthat␈α
␈↓↓gopher␈↓␈αmay␈αnot␈α
be␈αtotal␈αis␈αprovided␈α
for␈αby␈αnot␈α
assuming␈αthat␈α␈↓↓gopher x␈↓␈αis␈α
an
␈↓ ↓H␈↓S-expression␈αand␈αleaving␈αit␈αto␈αbe␈αproved␈αas␈αan␈αexpression␈αof␈αtermination.␈α The␈αtotal␈αcorrectess␈αof
␈↓ ↓H␈↓␈↓↓gopher␈↓ is then expressed by the formula

␈↓ ↓H␈↓3)␈↓ α8  ␈↓↓∀ x y.(issexp gopher[x.y] ∧ ␈↓αat␈↓↓ ␈↓αa␈↓↓ gopher[x.y] ∧ fringe gopher[x.y] = fringe[x.y])␈↓,

␈↓ ↓H␈↓where␈αthe␈αfirst␈αconjunct␈αsays␈αthat␈α␈↓↓gopher[x.y]␈↓␈αis␈αan␈αS-expression,␈α(i.e.␈αthat␈α␈↓↓gopher␈↓␈αis␈αtotal␈αon␈αnon-
␈↓ ↓H␈↓atoms),␈αthe␈α
second␈αsays␈α
that␈αits␈α␈↓↓car␈↓␈α
is␈αatomic␈α
(which␈αactually␈αimplies␈α
totality),␈αand␈α
the␈αlast␈αsays␈α
that
␈↓ ↓H␈↓gopher doesn't change the fringe.

␈↓ ↓H␈↓␈↓ α_(3) is readily proved by structural induction using the predicate

␈↓ ↓H␈↓4)␈↓ α8  ␈↓↓P(x) ≡ ∀y.(issexp gopher[x.y] ∧ ␈↓αat␈↓↓ ␈↓αa␈↓↓ gopher[x.y] ∧ fringe gopher[x.y] = fringe[x.y])␈↓,

␈↓ ↓H␈↓structural induction being expressed by the axiom schema

␈↓ ↓H␈↓5)␈↓ α8 ␈↓↓∀x.(␈↓αat␈↓↓ x ⊃ P(x)) ∧ ∀x.(¬␈↓αat␈↓↓ x ∧ P(␈↓αa␈↓↓ x) ∧ P(␈↓αd␈↓↓ x) ⊃ P(x)) ⊃ Nx.P(x)␈↓.

␈↓ ↓H␈↓␈↓ α_The␈α⊂proof␈α⊂uses␈α∂the␈α⊂first␈α⊂order␈α∂axioms␈α⊂for␈α⊂the␈α∂Lisp␈α⊂functions,␈α⊂the␈α∂associativity␈α⊂of␈α⊂the␈α∂*
␈↓ ↓H␈↓connective, and the formula

␈↓ ↓H␈↓6)␈↓ α8  ␈↓↓∀x y.(fringe[x.y] = fringe x * fringe y)␈↓

␈↓ ↓H␈↓which␈α
follows␈αimmediately␈α
from␈α
the␈αfirst␈α
order␈α
formula␈αdefining␈α
␈↓↓fringe␈↓␈α
once␈αit␈α
has␈α
been␈αproved
␈↓ ↓H␈↓(by structural induction) that ␈↓↓fringe␈↓ is total.

␈↓ ↓H␈↓␈↓ α_A␈α
formal␈αproof␈α
in␈α
the␈αFOL␈α
proof␈αchecker␈α
(Weyhrauch␈α
197x)␈αinvolves␈α
yyy␈α
steps␈αrequiring
␈↓ ↓H␈↓the typing of zzz characters to the proof checker.

␈↓ ↓H␈↓␈↓ α_The␈α⊃correctness␈α⊃of␈α∩␈↓↓samefringe␈↓␈α⊃itself␈α⊃is␈α∩longer␈α⊃to␈α⊃state␈α∩and␈α⊃prove,␈α⊃because␈α∩they␈α⊃involve
␈↓ ↓H␈↓simultaneous␈α
recursions␈α
and␈α
because␈α
we␈α
need␈α
two␈α
flavors␈α
of␈α
Boolean␈α
connectives␈α
-␈α
the␈α
ordinary
␈↓ ↓H␈↓ones␈α⊂and␈α⊃continuous␈α⊂ones␈α⊃that␈α⊂take␈α⊃values␈α⊂in␈α⊂a␈α⊃domain␈α⊂␈↓	P␈↓ = {T,F,␈↓	w␈↓},␈α⊃where␈α⊂␈↓	w␈↓␈α⊃represents␈α⊂the
␈↓ ↓H␈↓undefined element.